Nuprl Lemma : w-action-dec_wf
11,40
postcript
pdf
i
:Id,
TA
:(Id
Id
Type),
M
:(IdLnk
Id
Type). w-action-dec(
TA
;
M
;
i
)
Knd
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
w-action-dec(
TA
;
M
;
i
)
,
x
.
t
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
(
s
)
,
x
(
s1
,
s2
)
Lemmas
kindcase
wf
,
ifthenelse
wf
,
eq
id
wf
,
ldst
wf
,
IdLnk
wf
,
Knd
wf
,
Id
wf
origin
i:Id, TA:(Id
IdType), M:(IdLnkIdType). w-action-dec(TA;M;i) 
KndType i:Id, TA:(IdIdType), M:(IdLnkIdType). w-action-dec(TA;M;i) KndType x:A. B(x) T
x. t(x)x,y. t(x;y)